(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Import Reals.
Open Scope R_scope.
Require Export Matrix.Mat.RMatrix.
Require Export Matrix.Mat.RMtacs.

(** Sb -> Sa *)

(* 迎角 α  (angle of attack) *)
Parameter alpha : R.

(* 侧滑角β (sidelip angle) *)
Parameter beta : R.

(* 由 机体坐标轴系 Sb 转动迎角 α 到稳定坐标轴系 Ss 的转换矩阵 *)
Definition coordinate_transform_SbSs : Mat R 3 3 := mkMat_3_3
  (cos alpha)   0  (sin alpha)
       0        1       0
  (-sin alpha)  0  (cos alpha).

(* 由  稳定坐标轴系(Ss)  转动侧滑角β到 气流坐标轴系(Sa) *)
Definition coordinate_transform_SsSa : Mat R 3 3 := mkMat_3_3
  (cos beta )  (sin beta)  0
  (-sin beta)  (cos beta)  0
       0            0      1.

Definition coordinate_transform_SbSa : Mat R 3 3 := mkMat_3_3
  ((cos alpha)*(cos beta))  (sin beta) ((sin alpha)*(cos beta))
  (-(cos alpha)*(sin beta)) (cos beta) (-(sin alpha)*(sin beta))
   (- sin alpha)                 0           (cos alpha).

(* multiplication of SbSs and SsSa *)
Definition mul_SsSa_SbSs := 
  RMmul coordinate_transform_SsSa coordinate_transform_SbSs.

(* verify SsSa * SbSs = SbSa *)
Lemma SsSa_mul_SbSs_eq_SbSa : 
    mul_SsSa_SbSs === coordinate_transform_SbSa.
Proof.
  unfold mul_SsSa_SbSs.
  unfold coordinate_transform_SbSa.
  RMat_mul_simpl. unfold mkMat_3_3'.
  f_equal2. ring. f_equal2. ring.
  f_equal. ring. f_equal2. ring.
Qed.